Left Termination of the query pattern
deriv(a,g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 CutEliminatorProof (⇒, 0 ms)
↳2 Prolog
↳3 UndefinedPredicateHandlerProof (⇒, 0 ms)
↳4 Prolog
↳5 PrologToPiTRSProof (⇒, 59 ms)
↳6 PiTRS
↳7 RisEmptyProof (⇔, 0 ms)
↳8 YES

(0) Obligation:

Clauses:

d(+(U, V), X, +(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(-(U, V), X, -(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(!, ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU)))).
d(-(U), X, -(DU)) :- ','(!, d(U, X, DU)).
d(exp(U), X, *(exp(U), DU)) :- ','(!, d(U, X, DU)).
d(log(U), X, /(DU, U)) :- ','(!, d(U, X, DU)).
d(X, X, 1) :- !.
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).

Query: deriv(a,g,g)

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, 1).
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).

Query: deriv(a,g,g)

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, 1).
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).
integer(X0).
is(X0, X1).
write(X0).

Query: deriv(a,g,g)

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
R is empty.
Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

Pi-finite rewrite system:
R is empty.
Pi is empty.

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) YES